| Definitions | x:A  B(x), P   Q,  x:A. B(x), a < b, Void, False,  A, A  B, Id,  , t  T, {x:A| B(x)} ,  , Knd, #$n, True, (x l), KindDeq, deq-member(eq;x;L),  b, Type,  , P  Q, x:A  B(x), P & Q, P Q, {T}, f(x), x dom(f), z != f(x) P(a;z), M.rframe(k reads x), MsgA, , if b then t else f fi ,  , w.T, f(a), s = t, w.TA,  x.A(x), <a, b>, product-deq(A;B;a;b), E, Msg, type List, Unit, left + right, hasloc(k;i), A c B, mk-ma, x : v, f(x)?z, only members of L read x, M.ds(x), M.bframe(k sends on l), M(i), @i: only members of L read x, M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s), M.init(x,v), PossibleWorld(D;w), time(e), es-T(es), es-Choose(es), es-V(es), es-M(es), es-Send(es), es-Trans(es), es_vartype(es;i;x), Choose(i), kindtype(i;k), Send(i), s1  s2 mod x@i, Trans(i), es_state(es;i), es-independent(es;i;k;x), ES(the_w), FairFifo, World, D realizes2 es.P(es), es is an event system of D, ES,  x. t(x), D realizes es. P(es), vartype(i;x), Msg(M), Msg, locl(a), S  T, IdLnk, w.M, suptype(S; T), rcv(l,tg), outr(x),  b,  , a = b, tag(k), lnk(k), act(k), islocal(k), isrcv(k), kindcase(k; a.f(a); l,t.g(l;t) ), w-kindtype(TA;M;i), w-automaton(T;TA;M), w-machine(w;i), w-machine-independent(w;i;k;x) |